; Copyright (c) 2017 Microsoft Corporation
; issue #721
(set-option :smt.string_solver seq)
(set-option :model_validate true)
(declare-fun c0 () Bool)
(declare-fun c1 () String)
(define-fun e2 () String (ite c0 c1 ""))
(define-fun e3 () (RegEx String) (re.+ (re.range "0" "9")))
(assert (str.in.re e2 e3))
(assert (not (= "" e2)))
(check-sat)
;(get-model)
(reset)
(exit)
(set-option :smt.string_solver z3str3)
(set-option :model_validate true)
(declare-fun c0 () Bool)
(declare-fun c1 () String)
(define-fun e2 () String (ite c0 c1 ""))
(define-fun e3 () (RegEx String) (re.+ (re.range "0" "9")))
(assert (str.in.re e2 e3))
(assert (not (= "" e2)))
(check-sat)
;(get-model)